00100 GIVEAX(COND1,(∀ P)(∀ X)(∀ Y)(P⊃(IF P THEN X ELSE Y)=X)); 00200 00300 GIVEAX(COND2,(∀ P)(∀ X)(∀ Y)(¬P⊃(IF P THEN X ELSE Y)=Y)); 00400 01000 END;